// ==++==
// 
//   Copyright (c) Microsoft Corporation.  All rights reserved.
// 
// ==--==

using System;
using System.Collections.Generic;
using System.Text;
using Microsoft.Pex.Engine;
using Microsoft.ExtendedReflection.Metadata;
using Microsoft.ExtendedReflection.Interpretation;
using Microsoft.ExtendedReflection.Interpretation.MethodInterpretation;
using Microsoft.ExtendedReflection.Reasoning.ExecutionNodes;
using Microsoft.ExtendedReflection.Reasoning.Domains;
using Microsoft.ExtendedReflection.Interpretation.Visitors;
using Microsoft.ExtendedReflection.Collections;
using Microsoft.ExtendedReflection.Interpretation.States;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using Microsoft.ExtendedReflection.Interpretation.Effects;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.ExtendedReflection.ComponentModel;
using Microsoft.Pex.Engine.PostAnalysis;
using Microsoft.Pex.Engine.Drivers;
using Microsoft.ExtendedReflection.Utilities.Safe;

namespace DySy.Engine
{
    /// <summary>
    /// First main DySys class
    /// Analyzes method call stack, one height at a time.
    /// </summary>
    internal sealed class DySyPathAnalyzer
        : PexPathComponentBase
        , IService
    {
        DySyManager dySyManager;
        private TermManager TermManager
        {
            get { return this.ExplorationServices.TermManager; }
        }

        TermSimplifier simplifier;
        ThisNormalizer thisNormalizer;

        protected override void Initialize()
        {
            this.dySyManager = this.GetService<DySyManager>();
            this.simplifier = new TermSimplifier(this.TermManager, true);
            this.thisNormalizer = new ThisNormalizer(this.TermManager);
        }

        public override void Dispose()
        {
            if (this.thisNormalizer != null)
            {
                this.thisNormalizer.Dispose();
                this.thisNormalizer = null;
            }
            if (this.simplifier != null)
            {
                this.simplifier.Dispose();
                this.simplifier = null;
            }
            base.Dispose();
        }


        /// <summary>
        /// Analyze method invocations, one stack height at a time.
        /// Start with height zero (entry method).
        /// Next analyze all direct method calls from the entry method.
        /// Continue with level two calls.
        /// ...
        /// Until reach maximum method call height (of program or hardcoded DySy limit).
        /// </summary>
        /// <remarks>
        /// Analyze means to reset the path-condition (to track the method's pre-condition) 
        /// and to replace the method parameters and fields of the declaring class with 
        /// symbolic variables (to track the method's effects or post-condition).
        /// </remarks>
        public void Analyze()
        {
            this.Log.LogMessage(
                DySyLogCategories.DySy,
                "begin");

            int framesCount = 0;    // method invocations in testee
            int framesHandled = 0;  // method invocations handled
            int maxLevelCount = this.dySyManager.Options.MaxStackDepth; // user limit for method stack height
            for (int level = 0; level < maxLevelCount; level++)
            {
                InvocationPathConditionCollector controller = new InvocationPathConditionCollector(this, level);
                using (IEngine trackingEngine = this.PathServices.TrackingEngineFactory.CreateTrackingEngine(controller))
                {
                    IPexTrackingDriver driver = trackingEngine.GetService<IPexTrackingDriver>();
                    if (!driver.Run())  // (re-) run testee, tracking method stack height = level
                        break;
                }
                framesCount = SafeMath.Max(framesCount, controller.FramesCount);
                framesHandled += controller.FramesHandled;
                if (framesHandled > framesCount) framesHandled = framesCount;
                this.Log.LogMessage(
                    DySyLogCategories.DySy,
                    "collecting data, {0:P} of all frames up to level {1} / {2}",
                    ((double)framesHandled / framesCount), level, maxLevelCount);
                if (controller.FramesHandled == 0 || // did we make any progress? What about native frames?
                    framesHandled >= framesCount) // or have we processed all frames there are?
                    break;
            }

            this.Log.LogMessage(
                DySyLogCategories.DySy,
                "pruning potential invariants");
            {
                IIndexable<TypeEx> types = this.dySyManager.GetTypes();
                InvariantDetector controller = new InvariantDetector();
                foreach (var type in types)
                    controller.SetPotentialInvariants(type, this.dySyManager.GetPotentialInvariants(type));
                using (IEngine trackingEngine = this.PathServices.TrackingEngineFactory.CreateTrackingEngine(controller))
                {
                    IPexTrackingDriver driver = trackingEngine.GetService<IPexTrackingDriver>();
                    if (driver.Run())
                        foreach (var type in types)
                            this.dySyManager.SetInvariants(type, controller.GetRemainingInvariants(type));
                }
            }

            this.Log.LogMessage(
                DySyLogCategories.DySy,
                "end");
        }

        #region Public Accessors
        // This is cached statically since it is just a metadata property.
        // This code is not in the offial metadata API, since it is a *heuristic*
        static Method[] noMethods = new Method[0];
        static SafeDictionary<Method, Method[]> publicAccessors = new SafeDictionary<Method, Method[]>();
        static Method[] getPublicAccessors(Method method)
        {
            Method[] res;
            if (!publicAccessors.TryGetValue(method, out res))
            {
                SafeList<Method> l = new SafeList<Method>();
                if (method.IsVisible(VisibilityContext.Exported))
                    l.Add(method);
                TypeEx dt;
                if (method.TryGetDeclaringType(out dt) &&
                    method.IsVirtual)
                {
                    Method interfaceMethod;
                    foreach (var interfaceType in dt.Interfaces)
                        if (interfaceType.IsVisible(VisibilityContext.Exported))
                            if (method.TryReverseVTableLookup(interfaceType, out @interfaceMethod))
                                l.Add(interfaceMethod);
                }
                if (l.Count == 0)
                    res = noMethods;
                else
                    res = l.ToArray();
            }
            return res;
        }
        #endregion

        /**
         * Contains only the "this" variable         
         */
        private bool containsOnlyThis(Term x)
        {
            using (ParameterCollector pc = new ParameterCollector(this.TermManager))
            {
                pc.VisitTerm(default(TVoid), x);
                if (pc.ContainsProperObject || pc.ContainsLoopVar)
                    return false;
                else
                    return this.containsOnlyThis(pc.Parameters);
            }
        }

        private bool containsOnlyThis(IEnumerable<Parameter> parameters)
        {
            foreach (var p in parameters)
                if (!p.IsThis)
                    return false;
            return true;
        }

        private IIndexable<Term> splitConjunction(Term conjunction)
        {
            if (this.TermManager.IsTrue(conjunction))
                return Indexable.Empty<Term>();

            IIndexable<Term> conjuncts;
            if (this.TermManager.TryGetLogicalAnd(conjunction, out conjuncts))
            {
                SafeDebug.Assert((this.TermManager.AreProperStackBooleans(conjuncts)), "(this.TermManager.AreProperStackBooleans(conjuncts))");
                return conjuncts;
            }
            else
                return Indexable.One(conjunction);
        }


        #region private classes
        /// <summary>
        /// ParameterCollector
        /// </summary>
        class ParameterCollector : TermInternalizingRewriter<TVoid>
        {
            Method method;
            SafeSet<Parameter> parameters;
            bool containsProperObject;
            bool containsLoopVar;

            public ParameterCollector(TermManager termManager)
                : base(termManager, OnCollection.Fail)
            {
                this.parameters = new SafeSet<Parameter>();
            }

            public Method Method
            {
                get { return this.method; }
            }

            public IEnumerable<Parameter> Parameters
            {
                get { return this.parameters; }
            }

            public bool ContainsProperObject
            {
                get { return this.containsProperObject; }
            }

            public bool ContainsLoopVar
            {
                get { return this.containsLoopVar; }
            }

            public override Term VisitSymbol(TVoid parameter, Term term, ISymbolId key)
            {
                ISymbolIdFromParameter fromParameter = key as ISymbolIdFromParameter;
                if (fromParameter != null &&
                    fromParameter.Parameter != null)
                {
                    Parameter p = fromParameter.Parameter;
                    Method m = p.DeclaringMember as Method;
                    if (m != null)
                    {
                        this.method = m;
                        this.parameters.Add(p);
                    }
                }

                if (key.GetType().Name == "LoopVarId") // TODO: Write better abstraction
                    this.containsLoopVar = true;

                return base.VisitSymbol(parameter, term, key);
            }

            public override Term VisitObject(TVoid parameter, Term term, IObjectId id, ObjectPropertyCollection properties)
            {
                object value;
                if (!this.TermManager.TryGetObject(term, out value))
                    this.containsProperObject = true;

                return base.VisitObject(parameter, term, id, properties);
            }
        }


        class InvocationPathConditionCollector
            : PexTrackingControllerBase
            , IEffectsTracker
        {
            DySyPathAnalyzer owner;
            int nextId;
            SafeSet<int> framesWithExceptions = new SafeSet<int>();
            SafeIntDictionary<int> undoMarkers = new SafeIntDictionary<int>();
            SafeIntDictionary<Term[]> derivedArguments = new SafeIntDictionary<Term[]>();
            int trackedFrameId; // method invocation frame tracked symbolically. if not tracking: -1
            SafeBag<Method> methodsOnStack = new SafeBag<Method>();
            SafeIntDictionary<int> oldDepths = new SafeIntDictionary<int>();
            int depth;  // method invocation stack height of current method invocation
            int level;  // track method invocation frames at this method invocation stack height
            int framesHandled;
            bool dirty;

            public InvocationPathConditionCollector(
                DySyPathAnalyzer owner,
                int level)
            {
                this.owner = owner;
                this.trackedFrameId = -1;
                this.level = level;
                this.depth = -1;
            }

            public int FramesCount
            {
                get { return this.nextId; }
            }

            public int FramesHandled
            {
                get { return this.framesHandled; }
            }

            #region PexTrackingControllerBase Members

            public override int GetNextFrameId(int threadId, Method method)
            {
                this.oldDepths[this.nextId] = this.depth;
                this.depth++;
                this.undoMarkers[this.nextId] = this.PathConditionBuilder.GetMarker();
                this.methodsOnStack.Add(method);
                return this.nextId++;
            }


            /// <summary>
            /// Replace current field values with symbolic variables, if we start
            /// tracking a method.
            /// </summary>
            public override PexArgumentTracking GetArgumentTreatment(PexTrackingThread thread, int frameId, Method method)
            {
                if (trackedFrameId >= 0)    // currently tracking execution symbolically
                    return PexArgumentTracking.Derived;
                else if (this.depth != this.level)  // not (yet) tracking symbolically
                    return PexArgumentTracking.Concrete;
                else  // start tracking symbolically
                {
                    this.PathConditionBuilder.Clear(); // let's start to collect that path condition from scratch
                    trackedFrameId = frameId; 

                    TypeEx declaringType;
                    if (method.TryGetDeclaringType(out declaringType))
                        foreach (var f in declaringType.DeclaredStaticFields)
                        {
                            Term symbol = this.TermManager.Symbol(
                                new PexTrackedStaticFieldId(f));
                            thread.State.StoreStaticField(f, symbol);
                        }

                    IState state = thread.State;
                    state.StartTrackingEffects(this); // Microsoft.ExtendedReflection.Interpretation.States.Impl.State
                    this.dirty = false;
                    this.newObjects.Clear();

                    return PexArgumentTracking.Track;
                }
            }

            public override void DerivedArguments(int frameId, Method method, Term[] arguments)
            {
                this.derivedArguments[frameId] = (Term[])arguments.Clone();
            }


            /// <summary>
            /// Done monitoring a method invocation.
            /// Store return value and effects on fields.
            /// </summary>
            public override void FrameDisposed(int frameId, PexTrackingFrame frame)
            {
                IThread thread = frame.Thread;
                IFrame caller = thread.CurrentFrame;
                Term[] arguments;

                if (frameId == trackedFrameId)
                {
                    this.framesHandled++;

                    Term pathCondition = this.PathConditionBuilder.Condition;
                    pathCondition = this.owner.thisNormalizer.VisitTerm(default(TVoid), pathCondition);
                    this.owner.dySyManager.AddPath(
                        frame.Method,
                        pathCondition); // add the local path condition to the set of known paths

                    TypeEx dt;
                    if (frame.Method.TryGetDeclaringType(out dt))
                    {
                        /* Look at each conjunct of the path condition we just observed for this method */
                        foreach (var conjunct in this.owner.splitConjunction(pathCondition))
                            if (this.owner.containsOnlyThis(conjunct))
                                this.owner.dySyManager.AddPotentialInvariant(
                                    dt,
                                    conjunct);
                    }

                    if (caller != null &&
                        caller.IsCallInProgress)
                    {
                        TypeEx declaringType;
                        if (frame.Method.TryGetDeclaringType(out declaringType))
                        {
                            foreach (var f in declaringType.DeclaredStaticFields)
                            {
                                // add static field updates to path results
                                Term fieldValue = thread.State.ReadStaticField(f);
                                processResult(frame, pathCondition, f, f.Type, fieldValue);
                            }

                            if (!frame.Method.IsStatic &&
                                declaringType.IsReferenceType &&
                                this.derivedArguments.TryGetValue(frameId, out arguments))
                            {
                                // add instance field results
                                Term receiver = frame.ReadArgument(0);
                                foreach (var f in declaringType.InstanceFields)
                                {
                                    Term fieldValue = thread.State.ReadObjectField(receiver, f);
                                    processResult(frame, pathCondition, f, f.Type, fieldValue);
                                }
                            }
                        }

                        // add call result
                        if (frame.Method.ResultType != SystemTypes.Void &&
                            caller.CallResultType != null &&
                            caller.CallResultType.Layout == frame.Method.ResultLayout)
                        {
                            Term result = caller.Pop();
                            processResult(frame, pathCondition, null, frame.Method.ResultType, result);
                            caller.Push(result);
                        }
                    }

                    IState state = thread.State;
                    state.EndTrackingEffects();
                    if (this.dirty)
                        this.owner.dySyManager.SetImpure(frame.Method);

                    this.trackedFrameId = -1;
                }

                if (this.trackedFrameId != -1 &&
                    !this.framesWithExceptions.Contains(frameId)) // TODO: This captures all frames in which exceptions occurred; but we should capture only those which propagate exceptions
                {
                    // when tracking, reduce calls to public methods to a function application merely representing the call
                    Method summarizedMethod = null;
                    if (this.methodsOnStack[frame.Method] > 1)
                        summarizedMethod = frame.Method;

                    Method[] publicAccessors = getPublicAccessors(frame.Method);
                    if (publicAccessors.Length > 0)
                        summarizedMethod = publicAccessors[0];

                    if (summarizedMethod != null)
                    {
                        this.PathConditionBuilder.Undo(this.undoMarkers[frameId]);
                        if (frame.Method.ResultType != SystemTypes.Void &&
                            this.derivedArguments.TryGetValue(frameId, out arguments))
                        {
                            if (caller != null &&
                                caller.IsCallInProgress &&
                                caller.CallResultType != null &&
                                caller.CallResultType.Layout == frame.Method.ResultLayout)
                            {
                                caller.Pop();
                                caller.Push(
                                    this.TermManager.Widen(
                                        this.TermManager.FunctionApplication(
                                            summarizedMethod,
                                            this.TermManager.Null,
                                            arguments),
                                        frame.Method.ResultType.StackWidening));
                            }
                        }
                    }
                }
                this.methodsOnStack.Remove(frame.Method);
                this.depth = this.oldDepths[frameId]; // this should just decrement depth, but in a more robust way
            }


            /// <summary>
            /// SzArrayIndexId
            /// </summary>
            class SzArrayIndexId : ISymbolId
            {
                public static readonly SzArrayIndexId Instance = new SzArrayIndexId();
                private SzArrayIndexId() { }

                #region ISymbolId Members

                public string Description
                {
                    get { return "$x"; }
                }

                public Layout Layout
                {
                    get { return Layout.I; }
                }

                public ObjectCreationTime ObjectCreationTime
                {
                    get { return ObjectCreationTime.Unknown; }
                }

                public Int64 GetPersistentHashCode()
                {
                    return 0; // TODO
                }
                #endregion
            }

            static readonly Term[] noIndices = new Term[0];

            /// <summary>
            /// Register array element update
            /// </summary>
            private void processResult(PexTrackingFrame frame, Term pathCondition, Field f, TypeEx type, Term fieldValue)
            {
                this.owner.dySyManager.AddPath(
                    frame.Method,
                    pathCondition,
                    f,
                    noIndices,
                    fieldValue);

                if (this.owner.dySyManager.Options.Arrays &&
                    type.Spec == TypeSpec.SzArray &&
                    !this.TermManager.IsDefaultValue(fieldValue))
                {
                    Term index = this.TermManager.Symbol(SzArrayIndexId.Instance);
                    Term elementValue = frame.Thread.State.ReadSzArrayElement(type.ElementType.Layout, fieldValue, index);
                    this.owner.dySyManager.AddPath(
                        frame.Method,
                        pathCondition,
                        f,
                        new Term[] { index },
                        this.TermManager.Widen(elementValue, type.ElementType.StackWidening));
                }
            }

            public override void FrameHasExplicitFailures(int frameId, Method method, IEnumerable<object> exceptionObjects)
            {
            }

            public override void FrameHasExceptions(int frameId, Method method)
            {
                this.framesWithExceptions.Add(frameId);
            }

            #endregion

            #region IEffectsTracker Members

            SafeSet<Term> newObjects = new SafeSet<Term>();
            void IEffectsTracker.AddNewObject(Term @object)
            {
                this.newObjects.Add(@object);
            }

            bool IEffectsTracker.IsNewObject(Term @object)
            {
                return this.newObjects.Contains(@object);
            }

            void IEffectsTracker.AddEffect(Method source, IEffect effect)
            {
            }

            void IEffectsTracker.ReadField(Method source, Field field)
            {
            }

            void IEffectsTracker.ReadFromMemoryRegion(Method source, UIntPtr baseAddress)
            {
            }

            void IEffectsTracker.WriteField(Method source, Field field)
            {
                this.dirty = true;
            }

            void IEffectsTracker.WriteToMemoryRegion(Method source, UIntPtr baseAddress)
            {
                this.dirty = true;
            }

            #endregion
        }

        class ThisNormalizer : TermInternalizingRewriter<TVoid>
        {
            public ThisNormalizer(TermManager termManager)
                : base(termManager, OnCollection.Fail)
            {
            }

            public override Term VisitSymbol(TVoid parameter, Term term, ISymbolId key)
            {
                ISymbolIdFromParameter parameterKey = key as ISymbolIdFromParameter;
                if (parameterKey != null &&
                    parameterKey.Parameter.IsThis)
                    return this.TermManager.Symbol(new ThisId(parameterKey.Parameter.Type));
                else
                    return base.VisitSymbol(parameter, term, key);
            }
        }

        class ThisRewriter : TermInternalizingRewriter<PexTrackingFrame>
        {
            bool initiallyDefault;
            public ThisRewriter(TermManager termManager, bool initiallyDefault)
                : base(termManager, OnCollection.Fail)
            {
                this.initiallyDefault = initiallyDefault;
            }


            /**
             * Instantiate method variable symbol with term passed to current invocation.
             */ 
            public override Term VisitSymbol(PexTrackingFrame parameter, Term term, ISymbolId key)
            {
                ThisId id = key as ThisId;
                TypeEx dt;
                if (id != null &&
                    !parameter.Method.IsStatic &&
                    parameter.Method.TryGetDeclaringType(out dt) &&
                    dt == id.Type)
                {
                    return parameter.ReadArgument(0);
                }

                Field instanceField;
                if (this.TermManager.TryGetInstanceField(term, out instanceField))
                    return ((PexTrackingState)parameter.Thread.State).ReadObjectFieldMap(instanceField);

                return base.VisitSymbol(parameter, term, key);
            }

            public override Term VisitSelect(PexTrackingFrame parameter, Term term, Term compound, Term index)
            {
                Term res = base.VisitSelect(parameter, term, compound, index);

                if (this.initiallyDefault)
                {
                    ISymbolId key;
                    if (this.TermManager.TryGetSymbol(index, out key))
                    {
                        ThisId id = key as ThisId;
                        if (id != null)
                        {
                            Term resCompound, resIndex;
                            Field instanceField;
                            if (this.TermManager.TryGetSelect(res, out resCompound, out resIndex) &&
                                this.TermManager.TryGetInstanceField(resCompound, out instanceField))
                                // TODO: refine.
                                return this.TermManager.Default(instanceField.Type.Layout);
                        }
                    }
                }

                return res;
            }
        }

        class InvariantDetector
            : PexTrackingControllerBase
        {
            int nextId;
            SafeDictionary<TypeEx, SafeSet<Term>> potentialInvariants = new SafeDictionary<TypeEx, SafeSet<Term>>();

            public InvariantDetector()
            {
            }

            public void SetPotentialInvariants(TypeEx type, IEnumerable<Term> potentialInvariants)
            {
                SafeSet<Term> s;
                if (!this.potentialInvariants.TryGetValue(type, out s))
                    this.potentialInvariants[type] = s = new SafeSet<Term>();
                s.AddRange(potentialInvariants);
            }

            public IEnumerable<Term> GetRemainingInvariants(TypeEx type)
            {
                SafeSet<Term> s;
                if (this.potentialInvariants.TryGetValue(type, out s))
                    return s;
                else
                    return Indexable.Empty<Term>();
            }

            #region ITrackingController Members

            public override int GetNextFrameId(int threadId, Method method)
            {
                return this.nextId++;
            }

            public override PexArgumentTracking GetArgumentTreatment(PexTrackingThread thread, int frameId, Method method)
            {
                return PexArgumentTracking.Concrete;
            }

            public override void DerivedArguments(int frameId, Method method, Term[] arguments)
            {
            }

            /**
             * End of monitored invocation.
             * Check if invariant candidates held in this invocation.
             * (in it's pre-condition (accumulated pc) and post-condition (effect on visible fields).
             */
            public override void FrameDisposed(int frameId, PexTrackingFrame frame)
            {
                TypeEx declaringType;
                if (!frame.Method.IsStatic &&
                    frame.Method.TryGetDeclaringType(out declaringType))
                {
                    SafeSet<TypeEx> emptyTypes = null;
                    foreach (SafeKeyValuePair<TypeEx, SafeSet<Term>> kvp in this.potentialInvariants)
                        if (declaringType.IsAssignableTo(kvp.Key))
                        {
                            TermManager termManager = ((PexTrackingState)frame.Thread.State).TermManager;
                            ThisRewriter tr = new ThisRewriter(termManager, false);
                            SafeSet<Term> violatedInvariants = null;
                            foreach (var potentialInvariant in kvp.Value)
                            {
                                /* Evaluate candidate invariant given pc and effects accumulated in frame */
                                Term evaluatedInvariant = tr.VisitTerm(frame, potentialInvariant);
                                if (!termManager.IsTrue(evaluatedInvariant))
                                {
                                    if (violatedInvariants == null)
                                        violatedInvariants = new SafeSet<Term>();
                                    violatedInvariants.Add(potentialInvariant);
                                }
                            }
                            if (violatedInvariants != null)
                                kvp.Value.RemoveRange(violatedInvariants);
                            if (kvp.Value.Count == 0)
                            {
                                if (emptyTypes == null)
                                    emptyTypes = new SafeSet<TypeEx>();
                                emptyTypes.Add(kvp.Key);
                            }
                        }
                    if (emptyTypes != null)
                        foreach (var t in emptyTypes)
                            this.potentialInvariants.Remove(t);
                }
            }

            public override void FrameHasExplicitFailures(int frameId, Method method, IEnumerable<object> exceptionObjects)
            {
            }

            public override void FrameHasExceptions(int frameId, Method method)
            {
            }
            #endregion
        }
        #endregion
    }
}
